T:Type, r:(TT). dec_binrel(T;x,y:T. x = y  T)  anti_sym(T;r)  (r >{T} ((r\))) 

latex

Up	gen algebra 1
Definitions of Statement	E >{T} E', x,y:T. E(x;y), dec_binrel(T;r), anti_sym(T;R), E, E\
Definitions	t  T, AntiSym(T;x,y.R(x;y)), E\, E, E >{T} E', anti_sym(T;R), x,y:T. E(x;y), dec_binrel(T;r), P  Q, , x:A. B(x), P & Q, P  Q, A, Dec(P), False
Lemmas	decidable wf, not wf